T:Type, eq:EqDecider(T), es:ES, x:Id, e:{e:E| @loc(e)(x:T)} .
((x changed before e))  ((x when e) = x initially@loc(e)   T) 

latex

Definitions	T, P & Q, @i(x:T), , True, t  T, P  Q, x:A. B(x), SqStable(P), P  Q, P  Q, ee'.P(e)
Lemmas	sq stable subtype rel, decidable assert, sq stable from decidable, es-when-init, es-init-le, es-init wf, deq wf, event system wf, Id wf, es-loc wf, es-dtype wf, es-E wf, changed wf, assert wf, not wf, not-changed